Section: New Results

Indistinguishability Proofs

Participants : Rohit Chadha, Vincent Cheval, Ştefan Ciobâcă, Hubert Comon-Lundh, Stéphanie Delaune, Steve Kremer.

Most existing results in verification of security protocols focus on trace properties such as secrecy or authentication. There are however several security properties that cannot be defined (or cannot be naturally defined) as trace properties and require the notion of indistinguishably. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography.

In the framework of the applied pi-calculus  [54] , as in similar languages based on equational logics, indistinguishability corresponds to a relation called trace equivalence. Roughly, two processes are trace equivalent when an observer cannot see any difference between the two processes.

Under some conditions, trace equivalence can be reduced to the problem of deciding symbolic equivalence, an equivalence relation introduced by M. Baudet  [55] . However, the procedure proposed by Mathieu Baudet for deciding symbolic equivalence is complex and cannot be implemented in its current state. Moreover, this method can only deal with simple processes with trivial else branches and is restricted to the class of subterm-convergent equational theories. Unfortunately, this makes it unsuitable for some case studies of interest to the SECSI team, among which the FOO electronic voting protocol, and the electronic passport protocols.

In order to provide tool support to decide trace equivalence, Rohit Chadha, Stefan Ciobâcă, and Steve Kremer propose a procedure that can handle a large set of cryptographic primitives. The procedure has been implemented in a prototype tool and has been effectively tested on examples (e.g., the FOO e-voting protocol). This paper is currently under submission.

Vincent Cheval, Hubert Comon-Lundh and Stéphanie Delaune have designed another procedure that allows one to check trace equivalence for a general class of processes [31] . In their class, they can model conditionals (with non-trivial else branches), private channels, and non-deterministic choice. The private authentication protocol and the various versions of the electronic passport protocol fall into their class.